w:World, e, e':E. FairFifo  (loc(e) = loc(e')  Id)  (e < e'  (time(e) < time(e'))) 

latex

Definitions	x:A. B(x), P  Q, P  Q, e < e', R^+, x:A. B(x), x f y, P & Q, P  Q, t  T, , rel_exp(T;R;n), , A  B, A, False, SQType(T), {T}, Y, if b then t else f fi , (i = j), ff, tt, , Dec(P), P  Q, , Unit, S  T,
Lemmas	nat plus wf, rel exp wf, nat plus inc, pred! wf, w-info wf, w-pred wf, w-time wf, nat wf, Id wf, loc wf, w-E wf, fair-fifo wf, world wf, nat plus properties, le wf, decidable int equal, w-pred!-decreases, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff